A:MsgA. AtomFree(da(A))  (l:IdLnk, tg:Id. AtomFree(Type;A.dout(l,tg))) 

latex

Definitions

t  T, x. t(x), x:A. B(x), Void, x.A(x), f(x)?z, x:AB(x), #$n, a<b, False, P  Q, A, AB, , {x:A| B(x) }, , Atom, x:AB(x), Id, IdLnk, left+right, type List, xdom(f). v=f(x)   P(x;v), f(a), nat-deq-aux, <a,b>, NatDeq, atom-deq-aux, AtomDeq, prod-deq(A;B;a;b), proddeq(a;b), product-deq(A;B;a;b), IdDeq, IdLnkDeq, sum-deq(A;B;a;b), sumdeq(a;b), union-deq(A;B;a;b), EqDecider(T), M.dout(l,tg), da(M), MsgA, AtomFree(d), rcv(l,tg), KindDeq, Type, Knd, a:A fp B(a), AtomFree(T;x)

Lemmas

Id wf, IdLnk wf, atom-free-decl wf, ma da wf, msga wf, atom-free-fpf, atom-free-Knd, rcv wf, fpf-cap wf, Kind-deq wf, fpf wf, Knd wf